D:Dsys.
Feasible(D)
 (dec:(j,b:IdM(j).state(M(j).da(locl(b))+Unit)).
 ((j, x, b:Id.
 ((M(j).rframe(locl(b) reads x)
 (( (s1, s2:M(j).state. (s1  s2 mod x)  dec(j,b,s1) = dec(j,b,s2)))
 (& d-chooser(D;dec)) 

latex

Definitions

x:A. B(x), P  Q, x:A. B(x), M.state, P & Q, A, d-chooser(D;dec), t  T, A & B, State(ds), if b t else f fi, x. t(x), Prop, true, false, SQType(T), {T}, S  T, S  T, b, isl(x), outl(x), P  Q, True, 1of(t), 2of(t), P  Q, Unit, (s1  s2 mod x), Dec(P), P  Q, , x(s), False, Feasible(D), Feasible(M), M.ds(x),

Lemmas

d-feasible-state, d-feasible-dec, ifthenelse wf, ma-no-read wf, d-m wf, locl wf, ma-ds wf, Id wf, pi1 wf, ma-da wf, ma-pre wf, pi2 wf, ma-has-pre wf, unit wf, it wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Id sq, assert-ma-no-read, ma-x-equiv wf, ma-rframe wf, ma-st wf, d-chooser wf, d-feasible wf, dsys wf, ma-feasible-ma-no-read, true wf, false wf